es:ES, T:Type, eq:EqDecider(T), v:T, x:Id, e:{e:E| @loc(e)(x:T)} ,
e':{e':E| e loc e'  & (x after e') = v} , a:E.
e loc a 
 ((x after a) = v)
 e''[e,a).((x after e'') = v)
 (a = next event in [e;e'] after which x = v) 

latex

Definitions	A, P  Q, P  Q, P  Q, A c B, x. t(x), , t  T, P  Q, e loc e' , P & Q, EqDecider(T), x:A. B(x), False, e[e1,e2).P(e), x(s), @i(x:T)
Lemmas	es-locl-total, es-next-assign wf, es-next-assign-property, assert wf, iff wf, bool wf, es-dtype wf, es-locl wf, es-le wf, es-le-loc, es-vartype wf, es-after wf, not wf, es-loc wf, Id wf, alle-between1 wf